1. $\uparrow$ff \\[0ex]$\vdash$ ff = tt